Dafny - Installation and Formal Verification of Smart Contracts

---

Slide 1: What is Dafny?

• Definition: Dafny is a programming language with built-in specification constructs that facilitate formal verification.
• Key Features:
  • Automatically verifies the correctness of programs based on pre- and post-conditions.
  • Integrates seamlessly with formal methods to ensure programs meet their specification.
  • Ideal for proving properties of smart contracts like correctness, safety, and fairness.

---

Slide 2: Why Use Dafny for Smart Contracts?

• Why Formal Verification is Critical:

  • Smart contracts, once deployed, cannot be easily altered, so verifying correctness beforehand is essential.
  • Formal verification ensures that smart contracts meet their specification under all possible inputs and scenarios.

• Advantages of Dafny:

  • Combines specification and programming into one language.
  • Enables developers to define preconditions, postconditions, and invariants, ensuring that smart contracts behave as expected.
  • Automatically checks logical correctness at compile time.

---

Slide 3: Installing Dafny

1. Pre-requisites:

   • .NET 6 SDK (for Windows, Linux, macOS).
   • Optionally, Visual Studio Code with Dafny extension for ease of development.

2. Installation Steps:

   1. Install .NET 6 SDK:

      • For Linux/Ubuntu:

        sudo apt install -y dotnet-sdk-6.0
        

      • For macOS:

        brew install --cask dotnet-sdk
        

      • For Windows:
        Download from: https://dotnet.microsoft.com/download

   2. Install Dafny via .NET:

      dotnet tool install -g dafny
      

   3. Verify Installation:

      dafny --version
      

3. Optional: Install Dafny Extension in Visual Studio Code:

   • Open Visual Studio Code.
   • Go to Extensions (Ctrl+Shift+X) and search for “Dafny”.
   • Install the extension for integrated Dafny support.

---

Slide 4: Dafny Basics

• Dafny Program Structure:

  • Methods: Define the functionality (like smart contract functions).
  • Preconditions: Specify the conditions that must be true before the method runs (e.g., user balance must be sufficient).
  • Postconditions: State what must hold true after the method execution (e.g., balances are updated correctly).
  • Invariants: Define properties that remain unchanged during the method’s execution.

• Formal Verification:

  • Dafny will attempt to prove the correctness of the method based on the preconditions and postconditions.
  • If any logical errors are found, Dafny will report them.

---

Slide 5: Formal Verification Using Dafny

• Key Concepts:

  1. Method Contracts:
     • Preconditions: Ensure that inputs meet required conditions.
     • Postconditions: Ensure that outputs and state changes meet expectations.
  2. Loop Invariants: Ensure that certain properties hold true within loops.
  3. Assertions: Allow you to specify properties that must be true at certain points in the code.

• Verification Workflow:

  1. Write the smart contract in Dafny.
  2. Define preconditions, postconditions, and invariants.
  3. Use Dafny to verify the correctness of the contract.
  4. Dafny generates a formal proof or provides counterexamples if verification fails.

---

Slide 6: Example Smart Contract: Simple Token Transfer

• Problem Statement:

  • A simple smart contract that transfers tokens between two accounts.

• Basic Dafny Method:

  method Transfer(sender: int, receiver: int, amount: int)
      requires sender != receiver
      requires amount > 0
      requires balance[sender] >= amount
      modifies balance
      ensures balance[sender] == old(balance[sender]) - amount
      ensures balance[receiver] == old(balance[receiver]) + amount
  {
      balance[sender] := balance[sender] - amount;
      balance[receiver] := balance[receiver] + amount;
  }
  

• Explanation:

  • Preconditions: Ensure the sender and receiver are different, and the sender has sufficient balance to transfer tokens.
  • Postconditions: Ensure the sender’s balance decreases by the transfer amount and the receiver’s balance increases accordingly.

---

Slide 7: Formalizing the Smart Contract in Dafny

• Defining Preconditions and Postconditions:

  • Preconditions guarantee that only valid inputs are allowed.
  • Postconditions guarantee that the method will behave correctly, ensuring that balances are updated properly after the transfer.

• Defining Invariants (optional):

  method Transfer(sender: int, receiver: int, amount: int)
      requires sender != receiver
      requires amount > 0
      requires balance[sender] >= amount
      modifies balance
      ensures balance[sender] == old(balance[sender]) - amount
      ensures balance[receiver] == old(balance[receiver]) + amount
      ensures forall i :: 0 <= i < balance.Length ==> balance[i] >= 0
  {
      balance[sender] := balance[sender] - amount;
      balance[receiver] := balance[receiver] + amount;
  }
  

• Explanation:

  • Invariant: Ensure that all balances remain non-negative after the transaction.

---

Slide 8: Running Formal Verification in Dafny

1. Verify the Contract:

   • In Visual Studio Code or from the terminal, run the verification command:

     dafny contract.dfy
     

2. Check Verification Output:

   • Dafny will either confirm that the contract satisfies all preconditions, postconditions, and invariants, or provide a counterexample if verification fails.

3. Interpret Dafny’s Output:

   • If any assertions or conditions are violated, Dafny will point out the specific line and provide details about the issue.

---